⊗⊗        inst[pat, expr, a] ← ⊗
⊗⊗            qif a = $$NO$ qthen $$NO$⊗
⊗⊗            qelse qif isvar pat qthen ⊗
⊗⊗                {assoc[pat, a]}[λz: ⊗
⊗⊗                    qif qn z qthen [pat . expr] . a⊗
⊗⊗                    qelse qif qd z = expr qthen a⊗
⊗⊗                    qelse $$NO$]⊗
⊗⊗            qelse qif qat pat qthen [qif pat = expr qthen a qelse $$NO$]⊗
⊗⊗            qelse qif qat expr qthen $$NO$⊗
⊗⊗            qelse inst[qd pat, qd expr, inst[qa pat, qa expr, a]]⊗



⊗⊗        instth[pat, exp, a] ← catch instth1[pat, exp, a]⊗



⊗⊗        instth1[pat, exp, a] ← ⊗
⊗⊗            if[isvar pat, ⊗
⊗⊗               {assoc[pat, a]}[λw: ⊗
⊗⊗                   if[qn w, [pat . exp] . a, qd w = exp, a, throw $$NO$]], ⊗
⊗⊗               qat pat, ⊗
⊗⊗               if[pat = exp, a, throw $$NO$], ⊗
⊗⊗               qat exp, ⊗
⊗⊗               throw $$NO$, ⊗
⊗⊗               instth1[qd pat, qd exp, instth1[qa pat, qa exp, a]]]⊗



⊗⊗        isvar x ← ⊗
⊗⊗            x⊗
⊗⊗            ε $$(X ⊗
⊗⊗               X0 ⊗
⊗⊗               X1 ⊗
⊗⊗               X2 ⊗
⊗⊗               Y ⊗
⊗⊗               Y0 ⊗
⊗⊗               Y1 ⊗
⊗⊗               Y2 ⊗
⊗⊗               Z ⊗
⊗⊗               Z0 ⊗
⊗⊗               Z1 ⊗
⊗⊗               Z2 ⊗
⊗⊗               U ⊗
⊗⊗               U0 ⊗
⊗⊗               U1 ⊗
⊗⊗               U2 ⊗
⊗⊗               V ⊗
⊗⊗               V0 ⊗
⊗⊗               V1 ⊗
⊗⊗               V2 ⊗
⊗⊗               W ⊗
⊗⊗               W0 ⊗
⊗⊗               W1 ⊗
⊗⊗               W2)⊗



⊗⊗        instp[pat, exp, a] ← ⊗
⊗⊗            if[isvar pat, ⊗
⊗⊗               {assoc[pat, a]}[λw: ⊗
⊗⊗                   [qn w ∧ [[pat . exp] . a]] ∨ [qd w = exp ∧ a]], ⊗
⊗⊗               qat pat, ⊗
⊗⊗               pat = exp ∧ a, ⊗
⊗⊗               ¬qat exp ∧ instp[qd pat, qd exp, instp[qa pat, qa exp, a]]]⊗



⊗⊗        match[expr, pattern] ← ⊗
⊗⊗            qprog [w]⊗
⊗⊗                 w ← inst[expr, pattern, qNIL]⊗
⊗⊗           $$LLLL:$ qif qat w qthen return w⊗
⊗⊗                 set[qaa w, qda w]⊗
⊗⊗                 w ← qd w⊗
⊗⊗                 qgo $$LLLL$⊗